\chapter{数据平面分布式验证数据划分和分布式模型研究}
\label{cha:distributed}
\section{数据平面模型}
数据平面验证的第一步是建立适合验证的数据平面模型（data plane model），其定义如下。
\begin{definition}
  数据平面模型。数据平面模型为一个三元组$M=\{V,H,T\}$，其中$V$为所有网络设备集合，$H$为数据平面所处理的包头集合，$T: H \times V \rightarrow 2^{H\times V}$为数据平面转发函数。
\end{definition}

\begin{definition}
\label{def:conflict-free-dpm}
  无冲突数据平面模型。令$M_i(V_i,H_i,T_i)$，$M_j(V_j,H_j,T_j)$为两个数据平面模型，如果$\forall (h,v) \in (H_i \cap H_j) \times (V_i \cap V_j): T_i(h,v)=T_j(h,v)$，则$M_i$和$M_j$是无冲突的数据平面模型。
\end{definition}

\begin{theorem}
\label{the:conflict-free-dpm}
  令$M_i(V_i,H_i,T_i)$，$M_j(V_j,H_j,T_j)$为两个数据平面模型，如果$V_i \cap V_j = \emptyset$ 或者$H_i \cap H_j = \emptyset$，则$M_i$和$M_j$为无冲突数据平面模型。
\end{theorem}
\begin{proof}
  根据定义\ref{def:conflict-free-dpm}，$(H_i \cap H_j) \times (V_i \cap V_j) = \emptyset$可直接证明。
\end{proof}

根据定理\ref{the:conflict-free-dpm}，现有工作Libra~\cite{zengLibra}和RCDC~\cite{jayaramanValidating2019}所构建的分布式模型均为无冲突数据平面模型，分别对应于包头空间互斥和设备空间互斥两种情况。

令$M_i(V_i,H_i,T_i)$，$M_j(V_j,H_j,T_j)$为两个无冲突数据平面模型，$M_{ij}=M_i \otimes M_j$，且：
\begin{equation}
\begin{aligned}
  V_{ij} = V_i \cup V_j\\
  H_{ij} = H_i \cup H_j\\
  T_{ij} = T_i \cup T_j
\end{aligned}
\end{equation}

然而，基于上述基础数据平面模型需要枚举所有包头，而且其验证过程需要对需求中的包头逐个进行验证，其算法复杂度为$O(|H|\times (|V|+|E|))$。为了实现更高效的验证过程，数据平面模型往往采用转发等价类来构建。

\begin{definition}
  数据平面转发等价类模型。数据平面转发等价类模型为一个三元组$\mathcal{M}(G,\mathcal{H},\mathcal{T})$，其中$G$为网络拓扑，$\mathcal{H}=2^H$为$H$的幂集，$\mathcal{T}: \mathcal{H} \times V \rightarrow \{G.V,2^{G.V}\}$，$V \times V \rightarrow \mathcal{T}$
\end{definition}

\section{分布式数据平面模型}
一个具有$k$个实例的集群形成一个包含$k$个局部数据平面模型（partial data plane model）的分布式数据平面模型。令$\mathbb{M}$为局部数据平面模型构成的集合，则$\mathbb{M}=\{M_1,...,M_k\}$。每个局部模型$M_i$有两个属性$M_i.H$和$M_i.V$，表示$M_i$由网络设备$M_i.V$上的转发规则构建，且$M_i$只考虑包头空间$M_i.H$。为了保证局部模型的完整性，令$M(v)=\{M_i|v \in M_i.V, M_i \in \mathbb{M}\}$，局部模型满足以下条件：
\begin{equation}
% \begin{split}
  \forall v \in V: \bigcup_{M \in M(v)} M.H = \mathbb{H}
  % \bigcup_{i=1}^k M_i.H = \mathbb{H}\\
  % \bigcup_{i=1}^k M_i.V = V
% \end{split}
\end{equation}

\begin{definition}
  数据平面模型连接。
\end{definition}

\begin{theorem}
  令$M$为全局模型，则$M=\bigotimes_{M \in \mathbb{M}} M$。
\end{theorem}

\begin{definition}
  拓扑相关的数据平面模型连接。
\end{definition}